COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.DEVICE XGP
C00004 00003	.MACRO B ⊂ BEGIN VERBATIM GROUP ⊃
C00008 00004	5Lead-in to Discussing AM System*
C00009 00005	HOW THE DEVELOPMENT MIGHT OCCUR
C00018 ENDMK
C⊗;
.DEVICE XGP

.FONT 1 "BASL30"
.FONT 2 "BASB30"
.FONT 4  "BASI30"
.FONT 5  "BDR40"
.FONT 6  "NGR25"
.FONT 7  "NGR20"
.FONT 8  "GRFX35"
.FONT A "SUP"
.FONT B "SUB"
.TURN ON "↑α↓_π[]{"
.TURN ON "⊗" FOR "%"
.TURN ON "@" FOR "%"
.PAGE FRAME 54 HIGH 89 WIDE
.TITLE AREA HEADING LINES 1 TO 2
.AREA TEXT LINES 4 TO 53
.COUNT PAGE PRINTING "1"
.TABBREAK
.ODDLEFTBORDER←EVENLEFTBORDER←850
.AT "ffi" ⊂ IF THISFONT ≤ 4 THEN "≠"  ELSE "fαfαi" ⊃;
.AT "ffl" ⊂ IF THISFONT ≤ 4 THEN "α∞" ELSE "fαfαl" ⊃;
.AT "ff"  ⊂ IF THISFONT ≤ 4 THEN "≥"  ELSE "fαf" ⊃;
.AT "fi"  ⊂ IF THISFONT ≤ 4 THEN "α≡" ELSE "fαi" ⊃;
.AT "fl"  ⊂ IF THISFONT ≤ 4 THEN "∨"  ELSE "fαl" ⊃;
.SELECT 1
.MACRO B ⊂ BEGIN VERBATIM GROUP ⊃
.MACRO E ⊂ APART END ⊃
.MACRO D ⊂ ONCE PREFACE 100 MILLS ⊃
.MACRO BB ⊂ BEGIN NOFILL SELECT 6 INDENT 0 GROUP PREFACE 0 ⊃
.MACRO BBB ⊂ BEGIN  INDENT 0,3,0  PREFACE 0  SINGLE SPACE ⊃
.MACRO BGIV ⊂ BEGIN NOFILL SELECT 7 INDENT 0 PREFACE 0  TURN OFF "{}" TURN ON "↑↓" ⊃
.MACRO B0 ⊂ BEGIN  WIDEN 2,7 SELECT 8 NOFILL PREFACE 0 MILLS TURN OFF "↑↓α"  GROUP ⊃
.MACRO B7 ⊂ BEGIN  WIDEN 7,7 SELECT 8 NOFILL PREFACE 0 MILLS TURN OFF "↑↓α"  GROUP ⊃
.MACRO W(F) ⊂ SELECT F NOFILL SINGLE SPACE; PREFACE 0; WIDEN 7,7 ⊃
.MACRO FAD ⊂ FILL ADJUST DOUBLE SPACE PREFACE 2 ⊃
.MACRO FAS ⊂ FILL ADJUST SINGLE SPACE PREFACE 1 ⊃
.FAD

.AT "[[" ⊂
[⊗4Slide: 
.⊃

.AT "]]" ⊂
⊗*]
.⊃

.MYFOOT←1
.FOOTSEP←"________________________________________________________________________________________"
.COUNT FOOTNOTE INLINE PRINTING "⊗A1⊗*"
.AT "$$" ENTRY "*" ⊂ XGENLINES←XGENLINES-1; NEXT FOOTNOTE; !;
.SEND FOOT ⊂ TURN ON "[]{" SELECT 7; SPACING 0; PREFACE 0; INDENT 0,10
⊗A{MYFOOT}⊗* ENTRY
.MYFOOT←MYFOOT+1
.BREAK ⊃ ⊃

.MACRO NSECP(A)  ⊂   SSECNUM←0
.SECNUM←SECNUM+1 
.SECTION←"A"
.SKIP TO COLUMN 1
.TURN ON "{∞→"   
.SEND CONTENTS ⊂
@1{SECNUM}. A⊗* ∞.→ {PAGE}
.⊃
.TURN OFF "{∞→"   
.ONCE CENTER TURN ON "{}"
@5↓_{SECNUM}. A_↓⊗*  
.  ⊃


.MACRO ASEC(A)  ⊂  SSECNUM←0
.SECTION←"A"
.SKIP TO COLUMN 1
.TURN ON "{∞→"   
.SEND CONTENTS ⊂
@1 A⊗*
.⊃
.TURN OFF "{∞→"   
.ONCE CENTER TURN ON "{}"
@5↓_A_↓⊗*  
.  ⊃


.MACRO NSEC(A)  ⊂  
.SSECNUM←0
.SECNUM←SECNUM+1 
.TURN ON "{∞→"   
.SEND CONTENTS ⊂
@1{SECNUM}. A⊗* ∞.→ {PAGE}
.⊃
.TURN OFF "{∞→"   
.SECTION←"A"
.GROUP SKIP 3
.ONCE CENTER TURN ON "{}"
@5↓_{SECNUM}. A_↓⊗*  
.  ⊃


.MACRO SSEC(A)  ⊂  TURN ON "{∞→"   
.SSECNUM←SSECNUM+1
.SSSECNUM←0
.SEND CONTENTS ⊂
@7               A⊗* ∞.→ {PAGE}
.⊃
.TURN OFF "{∞→"   
.ONCE INDENT 6 TURN ON "{}"
@2↓_{SECNUM}.{SSECNUM}. A_↓⊗*  
. ⊃

.MACRO ASSEC(A)  ⊂  TURN ON "{∞→"   
.SEND CONTENTS ⊂
@7               A⊗*
.⊃
.TURN OFF "{∞→"   
.ONCE INDENT 6 TURN ON "{}"
@2↓_A_↓⊗*  
. ⊃

.MACRO SSSEC(A)  ⊂  TURN ON "{∞→"   
.SSSECNUM←SSSECNUM+1
.TURN OFF "{∞→"   
.ONCE INDENT 1 TURN ON "{}"
@2↓_{SECNUM}.{SSECNUM}.{SSSECNUM}. A_↓⊗*  
. ⊃

.SECNUM←0
.SELECT 1
.PAGE←0
.PORTION THESIS
.NARROW 2,7
.TURN OFF "{∞→}"   
.PAGE←0
.NEXT PAGE
.INDENT 0
.FAD
.TURN OFF "{∞→}"   
.EVERY   HEADING(⊗7Beings:   Text   of  4IJCAI-75  Talk⊗*,Doug  Lenat,{DATE}    page {PAGE}⊗*)
⊗5Lead-in to Discussing AM System⊗*

Now that we've talked about math research, it's time to turn our
attention to how it might be automated. I'm going to describe a system,
AM, which is under construction now at SAIL, as my dissertation project.

First we'll see what AM is supposed to do, then a little of how it does it.

.SKIP TO COLUMN 1

.ONCE CENTER SELECT 5
HOW THE DEVELOPMENT MIGHT OCCUR

Time is running short, so let me just sketch for you a brief excerpt of
a session with AM:

SYSTEM: The relation TIMES↑-↑1 always sems to contain (n, (1,n)) and (n, (n,1)),
for all n. I have proved this. Investigating the class of those n for which
TIMES↑-↑1 contains no other pairs.

USER: Why?

SYSTEM: From a statement of the form ⊗6"∀xεX⊗*, at least P(x)", we can often find
an interesting subset of X as simply "{⊗6xεX  |⊗*  at most P(x)}".

In this case, AM has just discovered the set of prime numbers, and decided
that because of its definition, it is interesting enough to spend some time
studying it.

USER: Such numbers are called PRIME; each is a PRIME; the set is called PRIMES.

SYSTEM: ∀n, ∃1b, s.t. (n, b) ⊗6ε⊗* TIMES↑-↑1, and b is a bag solely of primes.

The system has now discovered the unique factorization theorem, as if by magic.
Let's look deeper and see how it managed this feat.

First we must see how knowledge is represented internally by AM.

<Show Being Families, Being parts, and then the list of Given Beings.>

Now, back to how AM conjectured the Unique Factorization Theorem.

(Section 5.2)

.SKIP TO COLUMN 1

After 5.2: 

To conclude, let me put up a few statistics about AM.
About 50 Beings are in AM already, and they have proposed some interesting
compositions, but I don't feel that AM is developed far enough to
talk about performance yet.  Hopefully a dissertation will be appearing
next summer, and we'll both then know what AM did.